i:Id, L:(Knd List), x:Id, t:Type. @i: only L affects x : t  Dsys 

latex

Definitions	x:A. B(x), t  T, Dsys, @i: only L affects x : t
Lemmas	ifthenelse wf, eqof wf, Id wf, id-deq wf, msga wf, ma-single-frame wf, ma-empty wf, Knd wf